$\forall$$A$:Type, $f$:($A$$\rightarrow$($A$ + Top)), $n$:$\mathbb{N}$, $y$:$A$.
\\[0ex]($\uparrow$can{-}apply($f$\^{}$n$;$y$)) $\Rightarrow$ ($\forall$$m$:$\mathbb{N}$. ($m$ $\leq$ $n$) $\Rightarrow$ ($\uparrow$can{-}apply($f$\^{}$m$;$y$)))